\begin{tabbing}
$\forall$$T$, $A$:Type, $P$:($A$$\rightarrow$$T$$\rightarrow\mathbb{B}$), $i$:Id, $k$:Knd.
\\[0ex]Normal($A$)
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ (($\uparrow$isrcv($k$)) $\Rightarrow$ ($i$ = destination(lnk($k$))))
\\[0ex]$\Rightarrow$ ($\neg$(locl("a") = $k$))
\\[0ex]$\Rightarrow$ $\vdash$${\it es}$.@$i$ \=$k$(v:$T$) triggers local action "a"\+
\\[0ex]when $P$ ("x":$A$) v
\-
\end{tabbing}